Nuprl Lemma : w-state-when
0,22
postcript
pdf
w
:World.
FairFifo
(
e
:E. state_when(
e
) = (
x
.s(loc(
e
);time(
e
)).
x
)
x
:Id
vartype(loc(
e
);
x
))
latex
Definitions
Id
,
t
T
,
x
:
A
.
B
(
x
)
,
time(
e
)
,
loc(
e
)
,
s(
i
;
t
).
x
,
x
.
A
(
x
)
,
vartype(
i
;
x
)
,
x
:
A
B
(
x
)
,
x
.
t
(
x
)
,
1of(
t
)
,
s
=
t
,
Prop
,
state_when(
e
)
,
E
,
P
Q
,
FairFifo
,
World
Lemmas
w-when-after
,
world
wf
,
fair-fifo
wf
,
w-E
wf
,
pi1
wf
,
w-vartype
wf
,
w-s
wf
,
w-loc
wf
,
w-time
wf
,
Id
wf
origin
w:World.
(e:E. state_when(e) = (
x.s(loc(e);time(e)).x) 
x:Id
vartype(loc(e);x)) w:World.
(e:E. state_when(e) = (x.s(loc(e);time(e)).x) x:Idvartype(loc(e);x)) Tx:A. B(x)x.A(x)B(x)
x. t(x) Q